package kodkod.analysis;

import java.util.*;

import kodkod.ast.*;
import kodkod.instance.TupleSet;

public class Leafs extends HashSet<Relation> {
	
	public static boolean includeAllQV = true;
	public static boolean includeExistQV = false;
	
	public Leafs() {
		super();
	}
	
	public Leafs(Expression exp) {
		super();
		
		if (exp instanceof UnaryExpression) {
			UnaryExpression e = (UnaryExpression)exp;
			this.addAll(new Leafs(e.expression()));
		}
		else if (exp instanceof BinaryExpression) {
			BinaryExpression e = (BinaryExpression)exp;
			this.addAll(new Leafs(e.left()));
			this.addAll(new Leafs(e.right()));
		}
		else if (exp instanceof NaryExpression) {
			NaryExpression e = (NaryExpression)exp;
			for (Expression child : e) {
				this.addAll(new Leafs(child));
			}
		}
		else if (exp instanceof Comprehension) {
			Comprehension e = (Comprehension)exp;
			for (Decl child : e.decls()) {
				this.addAll(new Leafs(child.expression()));
			}
		}
		else if (exp instanceof IfExpression) {
			IfExpression e = (IfExpression)exp;
			this.addAll(new Leafs(e.thenExpr()));
			this.addAll(new Leafs(e.elseExpr()));
		}
		else if (exp instanceof ProjectExpression) {
			ProjectExpression e = (ProjectExpression)exp;
			this.addAll(new Leafs(e.expression()));
		}
		else if (exp instanceof IntToExprCast) {
			IntToExprCast e = (IntToExprCast)exp;
		}
		else if (exp instanceof LeafExpression) {
			if (exp instanceof Relation) {
				Relation e = (Relation)exp;
				if (Analyzer.translation.primaryRelations.contains(e)) {
					this.add(e);
				}
			}
			else if (exp instanceof Variable) {
				Variable var = (Variable)exp;
				if (Analyzer.translation.skolemRelations.containsKey(var)) { 
					this.addAll(new Leafs(Analyzer.translation.skolemRelations.get(var)));
				} else if (includeAllQV && Analyzer.allDecls.containsKey(var)) {
					this.addAll(new Leafs(Analyzer.decls.get(var)));
				} else if (includeExistQV) {
					this.addAll(new Leafs(Analyzer.decls.get(var)));
				}
			}
//			else if (exp instanceof ConstantExpression) {}
		}
	}
	
	public Leafs(IntExpression exp) {
		super();
		
		if (exp instanceof UnaryIntExpression) {
			UnaryIntExpression e = (UnaryIntExpression)exp;
			this.addAll(new Leafs(e.intExpr()));
		} else if (exp instanceof BinaryIntExpression) {
			BinaryIntExpression e = (BinaryIntExpression)exp;
			this.addAll(new Leafs(e.left()));
			this.addAll(new Leafs(e.right()));
		} else if (exp instanceof NaryIntExpression) {
			NaryIntExpression e = (NaryIntExpression)exp;
			for (IntExpression child : e) this.addAll(new Leafs(child));
		} else if (exp instanceof SumExpression) {
			SumExpression e = (SumExpression)exp;
			this.addAll(new Leafs(((SumExpression) exp).intExpr()));
			for (Decl decl : e.decls()) this.addAll(new Leafs(decl.expression()));
		} else if (exp instanceof IfIntExpression) {
			IfIntExpression e = (IfIntExpression)exp;
			this.addAll(new Leafs(e.thenExpr()));
			this.addAll(new Leafs(e.elseExpr()));
		} else if (exp instanceof ExprToIntCast) {
			ExprToIntCast e = (ExprToIntCast)exp;
			this.addAll(new Leafs(e.expression()));
		} 
//		else if (exp instanceof IntConstant) {}
	}
}
